LeanMachineLearning exposition

ProbabilityTheory.«term𝓛[_|_;_]»🔗

Minimal Lean file

term𝓛[_|_;_]🔗

DefinitionProbabilityTheory.«term𝓛[_|_;_]»
Details

Law of Y conditioned on X.

🔗def
ProbabilityTheory.«term𝓛[_|_;_]» : Lean.ParserDescr
ProbabilityTheory.«term𝓛[_|_;_]» :
  Lean.ParserDescr

Code

notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ

Actions: Source · Open Issue